Corelab Seminar
2017-2018
Alex Kavvos
On the Semantics of Intensionality and Intensional Recursion
Abstract.
Intensionality is a phenomenon that occurs in logic and
computation. In the most general sense, a function is intensional
if it operates at a level finer than (extensional) equality. This
is a familiar setting for computer scientists, who often study
different programs or processes that are interchangeable, i.e.
extensionally equal, even though they are not implemented in the
same way, so intensionally distinct. Concomitant with
intensionality is the phenomenon of intensional recursion, which
refers to the ability of a program to have access to its own code.
This talk is concerned with crafting a logical toolkit through
which these phenomena can be studied. Our main contribution is a
framework in which mathematical and computational constructions
can be considered either extensionally, i.e. as abstract values,
or intensionally, i.e. as fine-grained descriptions of their
construction. The main tool in this is modal type theory, where we
use a modality to express intensionality in a programming
language. We then use category theory to provide a semantics for
the aforementioned language, through the novel notion of exposure.
The device of exposures is also useful in studying the interplay
between extension and intension, as well as in proving abstract
analogues of classic results with an intensional flavour, e.g.
Goedel's First Incompleteness Theorem, Tarski's Undefinability
Theorem, Rice's Theorem, and Kleene's Second Recursion Theorem.